import Mathlib

namespace CNVSStateRejection

/-- Stato astratto CNVS. -/
structure CNVSState where
  id : Nat

/--
Un candidato successore contiene uno stato
e una prova che esso è globalmente valido.
-/
structure ValidState (VGlobal : CNVSState → Prop) where
  state : CNVSState
  valid : VGlobal state

/--
Se uno stato non soddisfa `VGlobal`,
allora non può esistere un `ValidState`
che abbia quello stato come contenuto.
-/
theorem rejected_if_not_global_valid
    (VGlobal : CNVSState → Prop)
    (S' : CNVSState)
    (hReject : ¬ VGlobal S') :
    ¬ ∃ VS : ValidState VGlobal, VS.state = S' := by
  intro h
  rcases h with ⟨VS, hEq⟩
  subst hEq
  exact hReject VS.valid

/--
Esempio concreto:
lo stato con `id = 0` è valido,
lo stato con `id = 1` è rigettato.
-/
def ExampleVGlobal : CNVSState → Prop :=
  fun S => S.id = 0

def GoodState : CNVSState where
  id := 0

def BadState : CNVSState where
  id := 1

example :
    ExampleVGlobal GoodState := by
  rfl

example :
    ¬ ExampleVGlobal BadState := by
  unfold ExampleVGlobal BadState
  norm_num

example :
    ¬ ∃ VS : ValidState ExampleVGlobal,
        VS.state = BadState := by
  apply rejected_if_not_global_valid
  unfold ExampleVGlobal BadState
  norm_num

end CNVSStateRejection